$\forall$${\it es}$:ES, $P$:(E$\rightarrow\mathbb{P}$), $f$:(\{$e$:E$\mid$ $P$($e$)\} $\rightarrow$E).
\\[0ex]$f$ is locl{-}pre{-}preserving on $P$ $\Rightarrow$ Inj(\{$e$:E$\mid$ $P$($e$)\} ;E;$f$)